\begin{tabbing}
1. $T$ : Type
\\[0ex]2. $P$ : $T$$\rightarrow\mathbb{P}$
\\[0ex]3. $f$ : $\forall$$x$:$T$. Dec($P$($x$))
\\[0ex]4. $x$ : $T$
\\[0ex]$\vdash$  \=($\uparrow$isl(case $f$($x$) of inl($p$) =$>$ inr $p$  $\mid$ inr($p$) =$>$ inl $x$ ))\+
\\[0ex]$\Rightarrow$ (outl(case $f$($x$) of inl($p$) =$>$ inr $p$  $\mid$ inr($p$) =$>$ inl $x$ ) = $x$)
\-
\end{tabbing}